%==============================================================================
% Enunciado
%==============================================================================

% Formalizar en OTTER la siguiente argumentación y comprobar su validez:
% "En la oficina de Juan hay personas a las que le gusta la comida
% internacional. De hecho, Juan conoce a todos a los que le gusta la comida
% japonesa aunque no conoce a todos los que trabajan en su oficina. Por tanto,
% Juan conoce a alguien a quien le gusta la comida asiática."

%==============================================================================
% Formalización
%==============================================================================

set(binary_res).

formula_list(sos).
% En la oficina de Juan hay personas a las que le gusta la comida
% internacional. 
  exists x (gustaInternacional(x) & trabajaOficina(x,Juan)).

% De hecho, Juan conoce a todos a los que le gusta la comida japonesa.
  all x (gustaJaponesa(x) -> conoce(Juan,x)).

% no conoce a todos los que trabajan en su oficina.
  exists x (trabajoOficina(x,Juan) & (- conoce(Juan,x))).

% Conclusión: Juan conoce a alguien a quien le gusta la comida asiática.
  - (exists x (conoce(Juan,x) & gustaAsiatica(x))).

% Conocimiento Implícito:
% all x (gustaInternacional(x) -> gustaJaponesa(x)).
  all x (gustaInternacional(x) -> gustaAsiatica(x)).
  all x (gustaAsiatica(x) -> gustaJaponesa(x)).
  all x y (trabajaOficina(x,y) -> trabajaOficina(y,x)).

end_of_list.

%==============================================================================
